<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>PostScript</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/qc.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 4: QuickChick：用 Coq 进行基于性质的测试</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">PostScript</h1>


<div class="doc">

<div class="paragraph"> </div>

<a name="lab133"></a><h1 class="section">Future Directions</h1>

<div class="paragraph"> </div>

 We have lots of plans for future directions:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Automatic derivation of generators and shrinkers for data
         satisfying Inductive relations

</li>
<li> Vellum2 testing

</li>
<li> DeepSpec Web Server

</li>
<li> Testing-only variant of _Software Foundations_?

</li>
</ul>

<div class="paragraph"> </div>

<a name="lab134"></a><h1 class="section">Recommended Reading</h1>
 The material presented in this short course serves as an
    introduction to property based random testing using
    QuickChick. For the interested reader, we provide a few more
    references for additional reading:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The original QuickCheck paper by Koen Claessen and John Hughes
      from ICFP 2000.
      <a href="https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quick.pdf"><span class="inlineref">https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quick.pdf</span></a>

<div class="paragraph"> </div>


</li>
<li> The original QuickChick paper that focuses on a framework for
      proving the correctness of QuickChick generators.
      <a href="https://hal.inria.fr/hal-01162898/document"><span class="inlineref">https://hal.inria.fr/hal-01162898/document</span></a>

<div class="paragraph"> </div>


</li>
<li> A case study that uses QuickCheck to test non-interference for
      information-flow-control abstract machines.
      <a href="https://arxiv.org/abs/1409.0393v<sub>2</sub>"><span class="inlineref">https://arxiv.org/abs/1409.0393v<sub>2</sub></span></a>

<div class="paragraph"> </div>


</li>
<li> Code for that case study exists under the QuickChick
      organization of github (<a href="https://github.com/QuickChick"><span class="inlineref">https://github.com/QuickChick</span></a>) for
      both Haskell ("Testing Noninterference") and Coq ("IFC").

<div class="paragraph"> </div>


</li>
<li> A paper on deriving QuickChick generators for a large class of
      inductive relations.
      <a href="https://lemonidas.github.io/pdf/GeneratingGoodGenerators.pdf"><span class="inlineref">https://lemonidas.github.io/pdf/GeneratingGoodGenerators.pdf</span></a>

<div class="paragraph"> </div>


</li>
<li> Leo's PhD dissertation.
      <a href="https://lemonidas.github.io/pdf/Leo-PhD-Thesis.pdf"><span class="inlineref">https://lemonidas.github.io/pdf/Leo-PhD-Thesis.pdf</span></a>

</li>
</ul>
 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:19:02&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>